Nuprl Lemma : exists_over_and_r
13,42
postcript
pdf
T
:Type,
A
:
,
B
:(
T
). (
x
:
T
. (
A
&
B
(
x
)))
(
A
& (
x
:
T
.
B
(
x
)))
latex
Up
core
2
,
core
2
Definitions
t
T
,
P
Q
,
P
Q
,
x
(
s
)
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
origin
T:Type, A:
, B:(T
). (
x:T. (A & B(x))) 
(A & (x:T. B(x))) T:Type, A:, B:(T). (x:T. (A & B(x))) (A & (x:T. B(x))) 
T Q Qx:A. B(x) Qx:A. B(x)